A:Type. safety(A;L.no_repeats(A;L)) 

latex

Definitions	t  T, x:A. B(x), l1  l2, ||as||, P  Q, False, A, AB, , l[i], Prop, safety(A;tr.P(tr)), no_repeats(T;l), A & B, P & Q, P  Q, x:A. B(x), Y, {...i}, P  Q, b, ij, ij, {i...}, , a -- b
Lemmas	le to lt, ndiff zero, divisor bound, eq to le, mul cancel in le, le transitivity, le to lt weaken, int upper properties, minus mono wrt le, increasing le, assert of le int, add cancel in le, add mono wrt le, injection le, int lower properties, le wf, iseg length, iseg select, length wf1, nat wf, not wf, select wf, iseg wf